User blog:P進大好きbot/Whether Rayo's number is well-defined or not
Hi, everyone. I hope that you all are enojoying daily googology. First of all, I suspect that Rayo's number is not well-defined, even if one adds mathematically precise descriptions to the original definition. You know that Rayo wrote that the original definition is based on second order logic, but did not declare what axioms of second order logic the definition of Rayo's function is based on and what axioms of first order set theory the definition of the satisfaction relation used in the description of Rayo's function. Since we usually omit the declaration of axioms if we work in \(\textrm{ZFC}\) set theory, some googologists might guess that (the usual first order) \(\textrm{ZFC}\) set theory works here, and just ignore the fact that Rayo wrote that he used an unspecified second order logic. Also, some googologists state that Platonist universe work here. It is true that the second order logic seems to be replaced by \(\textrm{ZFC}\) set theory and then it is natural to consider the formalised \(\textrm{ZFC}\) axiom described by \(\textrm{FOST}\) for the satisfaction. Then I would like to consider another evidence which implies that Rayo's number is not well-defined even if we add the description of "\(\textrm{ZFC}\) set theory plus Platonist universe". The point is "the impossible reference to the Platonist universe of the coded theory in the base theory". Of course, my thought is possibly incorrect. I appreciate any opinions and corrections. To be more precise, I should have emphasised that I did not say that it is impossible to define Rayo's number under ANY formal system. It is quite obvious that it can be defined as long as a suitable expicit choice of second order logic is declared. Or, even (first order) \(\textrm{MK}\) set theory is sufficient. My statement is that \(\textrm{ZFC}\) set theory is not sufficient for this purpose, even if we allow to use a Platonist universe. =Definition= The definition of the notion of a definition in formal logic is explained in another blog post. In order to define a large number, one needs to write down (an abbreviation/interpretation by a natural language of) a formula \(\Phi\) of the base theory such that the formula \((\exists ! x(\Phi)) \wedge (\forall x(\Phi \to (x \in \mathbb{N})))\) of the base theory is provable. =Convention= In order to define a natural number, we need a formal theory in order to avoid serious ambiguity and paradoxes such as Berry's one. Of course, we can use a formal theory coded in a given formal theory. In order to distinguish them, I would like to call the formal theory in which we defined a large number the base theory and the theory defined in the base theory the coded theory. Rayo's number lies in the base theory by definition. Therefore Rayo's function should lie in the base theory, because so does its value. It implies that the domain of Rayo's function also lies in the base theory. On the other hand, the set theory given by the formal language \(\textrm{FOST}\) and some (not precisely declared) axioms is the coded theory. =Axiom= As I metioned above, I consider the case where both of the base theory and the coded theory are \(\textrm{ZFC}\) set theory. The reason why we need axioms in the base theory is explained in another blog post. The reason why we need axioms in the coded theory is because Rayo mentioned to the truth in the definition of the satisfaction function \(\textrm{Sat}\). The notion of the truth makes sense only when we consider a model, and the notion of a model makes sense only when we fix axioms. The definition of a model is explained in another blog post. =Satisfaction Relation= Now it is time to consider the function \(\textrm{Sat}\). It has two imputs \(\Phi\) and \(s\). The first imput \(\Phi\) is a coded formula, i.e. a formula of \(\textrm{FOST}\), which is a term (realised as a natural number or a formal sequence of letters) in the base theory. The second imput \(s\) is a variable assignment, which assings variables in \(\textrm{FOST}\) to natural numbers. The natural numbers are terms in the base theory, because Rayo's number, which lies in the base theory, is defined as the minimum of a certain set of them. In order to assign variables in the coded theory to natural numbers in the base theory, one needs to fix a correspondence from natural numbers in the base theory to formulae of the coded theory defining terms in the coded theory. Since we are working with \(\textrm{ZFC}\) set theory as the coded theory, there is a canonical choice. The well-known von Neuman construction yields a purel syntax-theoretical correspondence, as long as we assume the axiom of extensionality, the axiom of the empty set, the axiom of pairing, and the axiom of union for the coded set theory. In the definition of \(\textrm{Sat}\), Rayo mentioned to the truth, which is defined by the satisfaction at a model. Since Rayo's function uses \(\textrm{Sat}\) in order to define the set of namable natural numbers, the satisfaction should be a formula in the base theory so that the axiom of separation is applicable. Therefore the satisfaction should be either one of the following: * The formalised satisfaction at a set model \(M\). * The formalised satisfaction at a definable class model \(X\). On the other hand, there is no description of a set model \(M\) or a definable class model \(X\), and hence the only reasonable choice of a model is the definable class \(V\) of all sets in the coded theory. The reason why we are not allowed to use an unquantified unspecific set model \(M\) in the definition of a large number in the base theory is explained in another blog post. However, \(\Phi^V\) is equivalent to \(\Phi\) by definition, and hence the provability of \(\Phi^V\) is equivalent to that of \(\Phi\) under the coded theory. You know, the provability itself is too weak to define an uncomputable large number, because \(\textrm{ZFC}\) set theory is effectively axiomised, So this is not the right interpretation of the definition of Rayo's number. How can we define the satisfaction relation of a formula \(\Phi\) of the coded theory as a formula of the base theory without using the provability? OK. Some people believe that a Platonist universe might work here. =Platonist Universe= A Platonist universe is an abstract object in human mind which satisfies given axioms of set theory and whose informal existence people may or may not accept. It is not precisely defined in terms of pure mathematics because it is a philosophical notion, but is quite useful for us to avoid highly formal arguments on sets. Of course, the use of a Platonist universe is not the Almighty Universe, even though it is not precisely defined. I suspect that almost all googologists disagree with any statements such as "I am using the greatest Platonist universe, and hence I can regard \(\infty\) as a natural number! I win!!" or "My universe satisfies \(\perp\), and hence I can prove that my large number is bigger than whatever you will define!". Anyway, a Platonist universe is simply regarded as \(V\) in contexts in set theory. Then the truth at a Platonist universe just means the satisfaction at \(V\), and hence coincides with the provability. So a Platonist universe is not helpful, as long as we deal with it in a traditional way in mathematics. Should we deal with it as a purely philosophical notion? Even if we do so, it is an object which is not a term of the base theory. Then it is impossible for the base theory to refer to the truth in a Platonist universe. Therefore there is no way to apply the axiom of separation in order to define the set of namable natural numbers. As a result, the use of a Platonist universe does not work at all. = Alternative Direction? = Let \(V\) be a variable of the coded theory such that the axiom of the coded theory is precisely the union of the following two sets of all formulae; * A maximal consistent set \(\Sigma\) of formulae of the coded theory in which \(V\) never occurs and which contains the ZFC axiom. * The set \(\{\Phi^V \mid \Phi \in \Sigma\}\). I mean that I give up to use \(\textrm{ZFC}\) set theory as the coded theory. Of course, it is not so reasonable, because there is no declaration of the axiom in the original definition. This is not an affirmative interpretation of the definition of Rayo's number any more, but is the definition of a new large number. The provability of \(\Phi^V\) behaves as the truth. Indeed, since \(\Sigma\) is maximal, for any formula \(\Phi\) of the coded theory in which \(x\) does not occur, precisely one of \(\Phi^x\) and \((\neg(\Phi))^x = \neg(\Phi^x)\) is contained in the latter set of axioms. I note that such a \(\Sigma\) exists by Zorn's lemma in the base theory, as I proved in another blog post. Therefore the assumption that such \(V\) and \(\Sigma\) are given is not so harmful as the assumption that a Platonist universe is given. Using \(V\) under the axioms, we can formulate a Rayo-like large number, which is of course well-defined. I wrote more detailed explation of the use of a maximal consistent set of formulae in another blog post. Category:Blog posts